Left Termination of the query pattern
front(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 182 ms)
↳2 TRIPLES
↳3 UndefinedPredicateInTriplesTransformerProof (⇒, 0 ms)
↳4 TRIPLES
↳5 TriplesToPiDPProof (⇒, 229 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔, 0 ms)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇒, 0 ms)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔, 0 ms)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔, 0 ms)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇒, 0 ms)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔, 0 ms)
        ↳22 YES
    ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 9 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES

(0) Obligation:

Clauses:

front(void, []).
front(tree(X, void, void), .(X, [])).
front(tree(X1, L, R), Xs) :- ','(front(L, Ls), ','(front(R, Rs), app(Ls, Rs, Xs))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: front(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

pB(X1, X2, X3, X4, X5) :- frontD(X1, X2).
pB(X1, X2, X3, X4, X5) :- ','(frontcD(X1, X2), frontD(X3, X4)).
pB(X1, X2, X3, X4, X5) :- ','(frontcD(X1, X2), ','(frontcD(X3, X4), appC(X2, X4, X5))).
frontD(tree(X1, X2, X3), X4) :- pB(X2, X5, X3, X6, X4).
appC(.(X1, X2), X3, .(X1, X4)) :- appC(X2, X3, X4).
appE(.(X1, X2), X3, .(X1, X4)) :- appE(X2, X3, X4).
frontH(tree(X1, void, void), X2) :- ','(frontcF(X3), appA(X3, X2)).
frontH(tree(X1, void, tree(X2, X3, X4)), X5) :- pB(X3, X6, X4, X7, X8).
frontH(tree(X1, void, X2), X3) :- ','(frontcG(X2, X4), appA(X4, X3)).
frontH(tree(X1, tree(X2, void, void), X3), X4) :- frontD(X3, X5).
frontH(tree(X1, tree(X2, void, void), X3), .(X2, X4)) :- ','(frontcD(X3, X5), appA(X5, X4)).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- frontD(X3, X7).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), frontD(X4, X8)).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), ','(frontcD(X4, X8), appC(X7, X8, X9))).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), ','(frontcD(X4, X8), ','(appcC(X7, X8, X9), frontD(X5, X10)))).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), ','(frontcD(X4, X8), ','(appcC(X7, X8, X9), ','(frontcD(X5, X10), appE(X9, X10, X6))))).

Clauses:

appcA(X1, X1).
qcB(X1, X2, X3, X4, X5) :- ','(frontcD(X1, X2), ','(frontcD(X3, X4), appcC(X2, X4, X5))).
frontcD(void, []).
frontcD(tree(X1, void, void), .(X1, [])).
frontcD(tree(X1, X2, X3), X4) :- qcB(X2, X5, X3, X6, X4).
appcC([], X1, X1).
appcC(.(X1, X2), X3, .(X1, X4)) :- appcC(X2, X3, X4).
appcE([], X1, X1).
appcE(.(X1, X2), X3, .(X1, X4)) :- appcE(X2, X3, X4).
frontcF([]).
frontcG(void, []).
frontcG(tree(X1, void, void), .(X1, [])).
frontcG(tree(X1, X2, X3), X4) :- qcB(X2, X5, X3, X6, X4).

Afs:

frontH(x1, x2)  =  frontH(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [DT09].

(4) Obligation:

Triples:

pB(X1, X2, X3, X4, X5) :- frontD(X1, X2).
pB(X1, X2, X3, X4, X5) :- ','(frontcD(X1, X2), frontD(X3, X4)).
pB(X1, X2, X3, X4, X5) :- ','(frontcD(X1, X2), ','(frontcD(X3, X4), appC(X2, X4, X5))).
frontD(tree(X1, X2, X3), X4) :- pB(X2, X5, X3, X6, X4).
appC(.(X1, X2), X3, .(X1, X4)) :- appC(X2, X3, X4).
appE(.(X1, X2), X3, .(X1, X4)) :- appE(X2, X3, X4).
frontH(tree(X1, void, tree(X2, X3, X4)), X5) :- pB(X3, X6, X4, X7, X8).
frontH(tree(X1, tree(X2, void, void), X3), X4) :- frontD(X3, X5).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- frontD(X3, X7).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), frontD(X4, X8)).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), ','(frontcD(X4, X8), appC(X7, X8, X9))).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), ','(frontcD(X4, X8), ','(appcC(X7, X8, X9), frontD(X5, X10)))).
frontH(tree(X1, tree(X2, X3, X4), X5), X6) :- ','(frontcD(X3, X7), ','(frontcD(X4, X8), ','(appcC(X7, X8, X9), ','(frontcD(X5, X10), appE(X9, X10, X6))))).

Clauses:

appcA(X1, X1).
qcB(X1, X2, X3, X4, X5) :- ','(frontcD(X1, X2), ','(frontcD(X3, X4), appcC(X2, X4, X5))).
frontcD(void, []).
frontcD(tree(X1, void, void), .(X1, [])).
frontcD(tree(X1, X2, X3), X4) :- qcB(X2, X5, X3, X6, X4).
appcC([], X1, X1).
appcC(.(X1, X2), X3, .(X1, X4)) :- appcC(X2, X3, X4).
appcE([], X1, X1).
appcE(.(X1, X2), X3, .(X1, X4)) :- appcE(X2, X3, X4).
frontcF([]).
frontcG(void, []).
frontcG(tree(X1, void, void), .(X1, [])).
frontcG(tree(X1, X2, X3), X4) :- qcB(X2, X5, X3, X6, X4).

Afs:

frontH(x1, x2)  =  frontH(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
frontH_in: (b,f)
pB_in: (b,f,b,f,f)
frontD_in: (b,f)
frontcD_in: (b,f)
qcB_in: (b,f,b,f,f)
appcC_in: (b,b,f)
appC_in: (b,b,f)
appE_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FRONTH_IN_GA(tree(X1, void, tree(X2, X3, X4)), X5) → U9_GA(X1, X2, X3, X4, X5, pB_in_gagaa(X3, X6, X4, X7, X8))
FRONTH_IN_GA(tree(X1, void, tree(X2, X3, X4)), X5) → PB_IN_GAGAA(X3, X6, X4, X7, X8)
PB_IN_GAGAA(X1, X2, X3, X4, X5) → U1_GAGAA(X1, X2, X3, X4, X5, frontD_in_ga(X1, X2))
PB_IN_GAGAA(X1, X2, X3, X4, X5) → FRONTD_IN_GA(X1, X2)
FRONTD_IN_GA(tree(X1, X2, X3), X4) → U6_GA(X1, X2, X3, X4, pB_in_gagaa(X2, X5, X3, X6, X4))
FRONTD_IN_GA(tree(X1, X2, X3), X4) → PB_IN_GAGAA(X2, X5, X3, X6, X4)
PB_IN_GAGAA(X1, X2, X3, X4, X5) → U2_GAGAA(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U2_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U3_GAGAA(X1, X2, X3, X4, X5, frontD_in_ga(X3, X4))
U2_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → FRONTD_IN_GA(X3, X4)
U2_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U4_GAGAA(X1, X2, X3, X4, X5, frontcD_in_ga(X3, X4))
U4_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → U5_GAGAA(X1, X2, X3, X4, X5, appC_in_gga(X2, X4, X5))
U4_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → APPC_IN_GGA(X2, X4, X5)
APPC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U7_GGA(X1, X2, X3, X4, appC_in_gga(X2, X3, X4))
APPC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPC_IN_GGA(X2, X3, X4)
FRONTH_IN_GA(tree(X1, tree(X2, void, void), X3), X4) → U10_GA(X1, X2, X3, X4, frontD_in_ga(X3, X5))
FRONTH_IN_GA(tree(X1, tree(X2, void, void), X3), X4) → FRONTD_IN_GA(X3, X5)
FRONTH_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U11_GA(X1, X2, X3, X4, X5, X6, frontD_in_ga(X3, X7))
FRONTH_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → FRONTD_IN_GA(X3, X7)
FRONTH_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U12_GA(X1, X2, X3, X4, X5, X6, frontcD_in_ga(X3, X7))
U12_GA(X1, X2, X3, X4, X5, X6, frontcD_out_ga(X3, X7)) → U13_GA(X1, X2, X3, X4, X5, X6, frontD_in_ga(X4, X8))
U12_GA(X1, X2, X3, X4, X5, X6, frontcD_out_ga(X3, X7)) → FRONTD_IN_GA(X4, X8)
U12_GA(X1, X2, X3, X4, X5, X6, frontcD_out_ga(X3, X7)) → U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_in_ga(X4, X8))
U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_out_ga(X4, X8)) → U15_GA(X1, X2, X3, X4, X5, X6, appC_in_gga(X7, X8, X9))
U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_out_ga(X4, X8)) → APPC_IN_GGA(X7, X8, X9)
U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_out_ga(X4, X8)) → U16_GA(X1, X2, X3, X4, X5, X6, appcC_in_gga(X7, X8, X9))
U16_GA(X1, X2, X3, X4, X5, X6, appcC_out_gga(X7, X8, X9)) → U17_GA(X1, X2, X3, X4, X5, X6, frontD_in_ga(X5, X10))
U16_GA(X1, X2, X3, X4, X5, X6, appcC_out_gga(X7, X8, X9)) → FRONTD_IN_GA(X5, X10)
U16_GA(X1, X2, X3, X4, X5, X6, appcC_out_gga(X7, X8, X9)) → U18_GA(X1, X2, X3, X4, X5, X6, X9, frontcD_in_ga(X5, X10))
U18_GA(X1, X2, X3, X4, X5, X6, X9, frontcD_out_ga(X5, X10)) → U19_GA(X1, X2, X3, X4, X5, X6, appE_in_gga(X9, X10, X6))
U18_GA(X1, X2, X3, X4, X5, X6, X9, frontcD_out_ga(X5, X10)) → APPE_IN_GGA(X9, X10, X6)
APPE_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U8_GGA(X1, X2, X3, X4, appE_in_gga(X2, X3, X4))
APPE_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPE_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

frontcD_in_ga(void, []) → frontcD_out_ga(void, [])
frontcD_in_ga(tree(X1, void, void), .(X1, [])) → frontcD_out_ga(tree(X1, void, void), .(X1, []))
frontcD_in_ga(tree(X1, X2, X3), X4) → U24_ga(X1, X2, X3, X4, qcB_in_gagaa(X2, X5, X3, X6, X4))
qcB_in_gagaa(X1, X2, X3, X4, X5) → U21_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U21_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U22_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X3, X4))
U22_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → U23_gagaa(X1, X2, X3, X4, X5, appcC_in_gga(X2, X4, X5))
appcC_in_gga([], X1, X1) → appcC_out_gga([], X1, X1)
appcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U25_gga(X1, X2, X3, X4, appcC_in_gga(X2, X3, X4))
U25_gga(X1, X2, X3, X4, appcC_out_gga(X2, X3, X4)) → appcC_out_gga(.(X1, X2), X3, .(X1, X4))
U23_gagaa(X1, X2, X3, X4, X5, appcC_out_gga(X2, X4, X5)) → qcB_out_gagaa(X1, X2, X3, X4, X5)
U24_ga(X1, X2, X3, X4, qcB_out_gagaa(X2, X5, X3, X6, X4)) → frontcD_out_ga(tree(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
pB_in_gagaa(x1, x2, x3, x4, x5)  =  pB_in_gagaa(x1, x3)
frontD_in_ga(x1, x2)  =  frontD_in_ga(x1)
frontcD_in_ga(x1, x2)  =  frontcD_in_ga(x1)
frontcD_out_ga(x1, x2)  =  frontcD_out_ga(x1, x2)
U24_ga(x1, x2, x3, x4, x5)  =  U24_ga(x1, x2, x3, x5)
qcB_in_gagaa(x1, x2, x3, x4, x5)  =  qcB_in_gagaa(x1, x3)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x3, x6)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x2, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x4, x6)
appcC_in_gga(x1, x2, x3)  =  appcC_in_gga(x1, x2)
[]  =  []
appcC_out_gga(x1, x2, x3)  =  appcC_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x2, x3, x5)
qcB_out_gagaa(x1, x2, x3, x4, x5)  =  qcB_out_gagaa(x1, x2, x3, x4, x5)
appC_in_gga(x1, x2, x3)  =  appC_in_gga(x1, x2)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
FRONTH_IN_GA(x1, x2)  =  FRONTH_IN_GA(x1)
U9_GA(x1, x2, x3, x4, x5, x6)  =  U9_GA(x1, x2, x3, x4, x6)
PB_IN_GAGAA(x1, x2, x3, x4, x5)  =  PB_IN_GAGAA(x1, x3)
U1_GAGAA(x1, x2, x3, x4, x5, x6)  =  U1_GAGAA(x1, x3, x6)
FRONTD_IN_GA(x1, x2)  =  FRONTD_IN_GA(x1)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x3, x5)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x1, x3, x6)
U3_GAGAA(x1, x2, x3, x4, x5, x6)  =  U3_GAGAA(x1, x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x1, x2, x3, x6)
U5_GAGAA(x1, x2, x3, x4, x5, x6)  =  U5_GAGAA(x1, x3, x6)
APPC_IN_GGA(x1, x2, x3)  =  APPC_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4, x5)  =  U7_GGA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x4, x5, x7)
U12_GA(x1, x2, x3, x4, x5, x6, x7)  =  U12_GA(x1, x2, x3, x4, x5, x7)
U13_GA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GA(x1, x2, x3, x4, x5, x7)
U14_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GA(x1, x2, x3, x4, x5, x7, x8)
U15_GA(x1, x2, x3, x4, x5, x6, x7)  =  U15_GA(x1, x2, x3, x4, x5, x7)
U16_GA(x1, x2, x3, x4, x5, x6, x7)  =  U16_GA(x1, x2, x3, x4, x5, x7)
U17_GA(x1, x2, x3, x4, x5, x6, x7)  =  U17_GA(x1, x2, x3, x4, x5, x7)
U18_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_GA(x1, x2, x3, x4, x5, x7, x8)
U19_GA(x1, x2, x3, x4, x5, x6, x7)  =  U19_GA(x1, x2, x3, x4, x5, x7)
APPE_IN_GGA(x1, x2, x3)  =  APPE_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5)  =  U8_GGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

FRONTH_IN_GA(tree(X1, void, tree(X2, X3, X4)), X5) → U9_GA(X1, X2, X3, X4, X5, pB_in_gagaa(X3, X6, X4, X7, X8))
FRONTH_IN_GA(tree(X1, void, tree(X2, X3, X4)), X5) → PB_IN_GAGAA(X3, X6, X4, X7, X8)
PB_IN_GAGAA(X1, X2, X3, X4, X5) → U1_GAGAA(X1, X2, X3, X4, X5, frontD_in_ga(X1, X2))
PB_IN_GAGAA(X1, X2, X3, X4, X5) → FRONTD_IN_GA(X1, X2)
FRONTD_IN_GA(tree(X1, X2, X3), X4) → U6_GA(X1, X2, X3, X4, pB_in_gagaa(X2, X5, X3, X6, X4))
FRONTD_IN_GA(tree(X1, X2, X3), X4) → PB_IN_GAGAA(X2, X5, X3, X6, X4)
PB_IN_GAGAA(X1, X2, X3, X4, X5) → U2_GAGAA(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U2_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U3_GAGAA(X1, X2, X3, X4, X5, frontD_in_ga(X3, X4))
U2_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → FRONTD_IN_GA(X3, X4)
U2_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U4_GAGAA(X1, X2, X3, X4, X5, frontcD_in_ga(X3, X4))
U4_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → U5_GAGAA(X1, X2, X3, X4, X5, appC_in_gga(X2, X4, X5))
U4_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → APPC_IN_GGA(X2, X4, X5)
APPC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U7_GGA(X1, X2, X3, X4, appC_in_gga(X2, X3, X4))
APPC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPC_IN_GGA(X2, X3, X4)
FRONTH_IN_GA(tree(X1, tree(X2, void, void), X3), X4) → U10_GA(X1, X2, X3, X4, frontD_in_ga(X3, X5))
FRONTH_IN_GA(tree(X1, tree(X2, void, void), X3), X4) → FRONTD_IN_GA(X3, X5)
FRONTH_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U11_GA(X1, X2, X3, X4, X5, X6, frontD_in_ga(X3, X7))
FRONTH_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → FRONTD_IN_GA(X3, X7)
FRONTH_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U12_GA(X1, X2, X3, X4, X5, X6, frontcD_in_ga(X3, X7))
U12_GA(X1, X2, X3, X4, X5, X6, frontcD_out_ga(X3, X7)) → U13_GA(X1, X2, X3, X4, X5, X6, frontD_in_ga(X4, X8))
U12_GA(X1, X2, X3, X4, X5, X6, frontcD_out_ga(X3, X7)) → FRONTD_IN_GA(X4, X8)
U12_GA(X1, X2, X3, X4, X5, X6, frontcD_out_ga(X3, X7)) → U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_in_ga(X4, X8))
U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_out_ga(X4, X8)) → U15_GA(X1, X2, X3, X4, X5, X6, appC_in_gga(X7, X8, X9))
U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_out_ga(X4, X8)) → APPC_IN_GGA(X7, X8, X9)
U14_GA(X1, X2, X3, X4, X5, X6, X7, frontcD_out_ga(X4, X8)) → U16_GA(X1, X2, X3, X4, X5, X6, appcC_in_gga(X7, X8, X9))
U16_GA(X1, X2, X3, X4, X5, X6, appcC_out_gga(X7, X8, X9)) → U17_GA(X1, X2, X3, X4, X5, X6, frontD_in_ga(X5, X10))
U16_GA(X1, X2, X3, X4, X5, X6, appcC_out_gga(X7, X8, X9)) → FRONTD_IN_GA(X5, X10)
U16_GA(X1, X2, X3, X4, X5, X6, appcC_out_gga(X7, X8, X9)) → U18_GA(X1, X2, X3, X4, X5, X6, X9, frontcD_in_ga(X5, X10))
U18_GA(X1, X2, X3, X4, X5, X6, X9, frontcD_out_ga(X5, X10)) → U19_GA(X1, X2, X3, X4, X5, X6, appE_in_gga(X9, X10, X6))
U18_GA(X1, X2, X3, X4, X5, X6, X9, frontcD_out_ga(X5, X10)) → APPE_IN_GGA(X9, X10, X6)
APPE_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U8_GGA(X1, X2, X3, X4, appE_in_gga(X2, X3, X4))
APPE_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPE_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

frontcD_in_ga(void, []) → frontcD_out_ga(void, [])
frontcD_in_ga(tree(X1, void, void), .(X1, [])) → frontcD_out_ga(tree(X1, void, void), .(X1, []))
frontcD_in_ga(tree(X1, X2, X3), X4) → U24_ga(X1, X2, X3, X4, qcB_in_gagaa(X2, X5, X3, X6, X4))
qcB_in_gagaa(X1, X2, X3, X4, X5) → U21_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U21_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U22_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X3, X4))
U22_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → U23_gagaa(X1, X2, X3, X4, X5, appcC_in_gga(X2, X4, X5))
appcC_in_gga([], X1, X1) → appcC_out_gga([], X1, X1)
appcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U25_gga(X1, X2, X3, X4, appcC_in_gga(X2, X3, X4))
U25_gga(X1, X2, X3, X4, appcC_out_gga(X2, X3, X4)) → appcC_out_gga(.(X1, X2), X3, .(X1, X4))
U23_gagaa(X1, X2, X3, X4, X5, appcC_out_gga(X2, X4, X5)) → qcB_out_gagaa(X1, X2, X3, X4, X5)
U24_ga(X1, X2, X3, X4, qcB_out_gagaa(X2, X5, X3, X6, X4)) → frontcD_out_ga(tree(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
pB_in_gagaa(x1, x2, x3, x4, x5)  =  pB_in_gagaa(x1, x3)
frontD_in_ga(x1, x2)  =  frontD_in_ga(x1)
frontcD_in_ga(x1, x2)  =  frontcD_in_ga(x1)
frontcD_out_ga(x1, x2)  =  frontcD_out_ga(x1, x2)
U24_ga(x1, x2, x3, x4, x5)  =  U24_ga(x1, x2, x3, x5)
qcB_in_gagaa(x1, x2, x3, x4, x5)  =  qcB_in_gagaa(x1, x3)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x3, x6)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x2, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x4, x6)
appcC_in_gga(x1, x2, x3)  =  appcC_in_gga(x1, x2)
[]  =  []
appcC_out_gga(x1, x2, x3)  =  appcC_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x2, x3, x5)
qcB_out_gagaa(x1, x2, x3, x4, x5)  =  qcB_out_gagaa(x1, x2, x3, x4, x5)
appC_in_gga(x1, x2, x3)  =  appC_in_gga(x1, x2)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
FRONTH_IN_GA(x1, x2)  =  FRONTH_IN_GA(x1)
U9_GA(x1, x2, x3, x4, x5, x6)  =  U9_GA(x1, x2, x3, x4, x6)
PB_IN_GAGAA(x1, x2, x3, x4, x5)  =  PB_IN_GAGAA(x1, x3)
U1_GAGAA(x1, x2, x3, x4, x5, x6)  =  U1_GAGAA(x1, x3, x6)
FRONTD_IN_GA(x1, x2)  =  FRONTD_IN_GA(x1)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x3, x5)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x1, x3, x6)
U3_GAGAA(x1, x2, x3, x4, x5, x6)  =  U3_GAGAA(x1, x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x1, x2, x3, x6)
U5_GAGAA(x1, x2, x3, x4, x5, x6)  =  U5_GAGAA(x1, x3, x6)
APPC_IN_GGA(x1, x2, x3)  =  APPC_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4, x5)  =  U7_GGA(x1, x2, x3, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x4, x5, x7)
U12_GA(x1, x2, x3, x4, x5, x6, x7)  =  U12_GA(x1, x2, x3, x4, x5, x7)
U13_GA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GA(x1, x2, x3, x4, x5, x7)
U14_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GA(x1, x2, x3, x4, x5, x7, x8)
U15_GA(x1, x2, x3, x4, x5, x6, x7)  =  U15_GA(x1, x2, x3, x4, x5, x7)
U16_GA(x1, x2, x3, x4, x5, x6, x7)  =  U16_GA(x1, x2, x3, x4, x5, x7)
U17_GA(x1, x2, x3, x4, x5, x6, x7)  =  U17_GA(x1, x2, x3, x4, x5, x7)
U18_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U18_GA(x1, x2, x3, x4, x5, x7, x8)
U19_GA(x1, x2, x3, x4, x5, x6, x7)  =  U19_GA(x1, x2, x3, x4, x5, x7)
APPE_IN_GGA(x1, x2, x3)  =  APPE_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5)  =  U8_GGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 26 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPE_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPE_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

frontcD_in_ga(void, []) → frontcD_out_ga(void, [])
frontcD_in_ga(tree(X1, void, void), .(X1, [])) → frontcD_out_ga(tree(X1, void, void), .(X1, []))
frontcD_in_ga(tree(X1, X2, X3), X4) → U24_ga(X1, X2, X3, X4, qcB_in_gagaa(X2, X5, X3, X6, X4))
qcB_in_gagaa(X1, X2, X3, X4, X5) → U21_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U21_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U22_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X3, X4))
U22_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → U23_gagaa(X1, X2, X3, X4, X5, appcC_in_gga(X2, X4, X5))
appcC_in_gga([], X1, X1) → appcC_out_gga([], X1, X1)
appcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U25_gga(X1, X2, X3, X4, appcC_in_gga(X2, X3, X4))
U25_gga(X1, X2, X3, X4, appcC_out_gga(X2, X3, X4)) → appcC_out_gga(.(X1, X2), X3, .(X1, X4))
U23_gagaa(X1, X2, X3, X4, X5, appcC_out_gga(X2, X4, X5)) → qcB_out_gagaa(X1, X2, X3, X4, X5)
U24_ga(X1, X2, X3, X4, qcB_out_gagaa(X2, X5, X3, X6, X4)) → frontcD_out_ga(tree(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
frontcD_in_ga(x1, x2)  =  frontcD_in_ga(x1)
frontcD_out_ga(x1, x2)  =  frontcD_out_ga(x1, x2)
U24_ga(x1, x2, x3, x4, x5)  =  U24_ga(x1, x2, x3, x5)
qcB_in_gagaa(x1, x2, x3, x4, x5)  =  qcB_in_gagaa(x1, x3)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x3, x6)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x2, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x4, x6)
appcC_in_gga(x1, x2, x3)  =  appcC_in_gga(x1, x2)
[]  =  []
appcC_out_gga(x1, x2, x3)  =  appcC_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x2, x3, x5)
qcB_out_gagaa(x1, x2, x3, x4, x5)  =  qcB_out_gagaa(x1, x2, x3, x4, x5)
APPE_IN_GGA(x1, x2, x3)  =  APPE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPE_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPE_IN_GGA(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPE_IN_GGA(x1, x2, x3)  =  APPE_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPE_IN_GGA(.(X1, X2), X3) → APPE_IN_GGA(X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPE_IN_GGA(.(X1, X2), X3) → APPE_IN_GGA(X2, X3)
    The graph contains the following edges 1 > 1, 2 >= 2

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPC_IN_GGA(X2, X3, X4)

The TRS R consists of the following rules:

frontcD_in_ga(void, []) → frontcD_out_ga(void, [])
frontcD_in_ga(tree(X1, void, void), .(X1, [])) → frontcD_out_ga(tree(X1, void, void), .(X1, []))
frontcD_in_ga(tree(X1, X2, X3), X4) → U24_ga(X1, X2, X3, X4, qcB_in_gagaa(X2, X5, X3, X6, X4))
qcB_in_gagaa(X1, X2, X3, X4, X5) → U21_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U21_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U22_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X3, X4))
U22_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → U23_gagaa(X1, X2, X3, X4, X5, appcC_in_gga(X2, X4, X5))
appcC_in_gga([], X1, X1) → appcC_out_gga([], X1, X1)
appcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U25_gga(X1, X2, X3, X4, appcC_in_gga(X2, X3, X4))
U25_gga(X1, X2, X3, X4, appcC_out_gga(X2, X3, X4)) → appcC_out_gga(.(X1, X2), X3, .(X1, X4))
U23_gagaa(X1, X2, X3, X4, X5, appcC_out_gga(X2, X4, X5)) → qcB_out_gagaa(X1, X2, X3, X4, X5)
U24_ga(X1, X2, X3, X4, qcB_out_gagaa(X2, X5, X3, X6, X4)) → frontcD_out_ga(tree(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
frontcD_in_ga(x1, x2)  =  frontcD_in_ga(x1)
frontcD_out_ga(x1, x2)  =  frontcD_out_ga(x1, x2)
U24_ga(x1, x2, x3, x4, x5)  =  U24_ga(x1, x2, x3, x5)
qcB_in_gagaa(x1, x2, x3, x4, x5)  =  qcB_in_gagaa(x1, x3)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x3, x6)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x2, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x4, x6)
appcC_in_gga(x1, x2, x3)  =  appcC_in_gga(x1, x2)
[]  =  []
appcC_out_gga(x1, x2, x3)  =  appcC_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x2, x3, x5)
qcB_out_gagaa(x1, x2, x3, x4, x5)  =  qcB_out_gagaa(x1, x2, x3, x4, x5)
APPC_IN_GGA(x1, x2, x3)  =  APPC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

APPC_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPC_IN_GGA(X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPC_IN_GGA(x1, x2, x3)  =  APPC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APPC_IN_GGA(.(X1, X2), X3) → APPC_IN_GGA(X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APPC_IN_GGA(.(X1, X2), X3) → APPC_IN_GGA(X2, X3)
    The graph contains the following edges 1 > 1, 2 >= 2

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PB_IN_GAGAA(X1, X2, X3, X4, X5) → FRONTD_IN_GA(X1, X2)
FRONTD_IN_GA(tree(X1, X2, X3), X4) → PB_IN_GAGAA(X2, X5, X3, X6, X4)
PB_IN_GAGAA(X1, X2, X3, X4, X5) → U2_GAGAA(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U2_GAGAA(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → FRONTD_IN_GA(X3, X4)

The TRS R consists of the following rules:

frontcD_in_ga(void, []) → frontcD_out_ga(void, [])
frontcD_in_ga(tree(X1, void, void), .(X1, [])) → frontcD_out_ga(tree(X1, void, void), .(X1, []))
frontcD_in_ga(tree(X1, X2, X3), X4) → U24_ga(X1, X2, X3, X4, qcB_in_gagaa(X2, X5, X3, X6, X4))
qcB_in_gagaa(X1, X2, X3, X4, X5) → U21_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X1, X2))
U21_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X1, X2)) → U22_gagaa(X1, X2, X3, X4, X5, frontcD_in_ga(X3, X4))
U22_gagaa(X1, X2, X3, X4, X5, frontcD_out_ga(X3, X4)) → U23_gagaa(X1, X2, X3, X4, X5, appcC_in_gga(X2, X4, X5))
appcC_in_gga([], X1, X1) → appcC_out_gga([], X1, X1)
appcC_in_gga(.(X1, X2), X3, .(X1, X4)) → U25_gga(X1, X2, X3, X4, appcC_in_gga(X2, X3, X4))
U25_gga(X1, X2, X3, X4, appcC_out_gga(X2, X3, X4)) → appcC_out_gga(.(X1, X2), X3, .(X1, X4))
U23_gagaa(X1, X2, X3, X4, X5, appcC_out_gga(X2, X4, X5)) → qcB_out_gagaa(X1, X2, X3, X4, X5)
U24_ga(X1, X2, X3, X4, qcB_out_gagaa(X2, X5, X3, X6, X4)) → frontcD_out_ga(tree(X1, X2, X3), X4)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
frontcD_in_ga(x1, x2)  =  frontcD_in_ga(x1)
frontcD_out_ga(x1, x2)  =  frontcD_out_ga(x1, x2)
U24_ga(x1, x2, x3, x4, x5)  =  U24_ga(x1, x2, x3, x5)
qcB_in_gagaa(x1, x2, x3, x4, x5)  =  qcB_in_gagaa(x1, x3)
U21_gagaa(x1, x2, x3, x4, x5, x6)  =  U21_gagaa(x1, x3, x6)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x2, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x4, x6)
appcC_in_gga(x1, x2, x3)  =  appcC_in_gga(x1, x2)
[]  =  []
appcC_out_gga(x1, x2, x3)  =  appcC_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U25_gga(x1, x2, x3, x4, x5)  =  U25_gga(x1, x2, x3, x5)
qcB_out_gagaa(x1, x2, x3, x4, x5)  =  qcB_out_gagaa(x1, x2, x3, x4, x5)
PB_IN_GAGAA(x1, x2, x3, x4, x5)  =  PB_IN_GAGAA(x1, x3)
FRONTD_IN_GA(x1, x2)  =  FRONTD_IN_GA(x1)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x1, x3, x6)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PB_IN_GAGAA(X1, X3) → FRONTD_IN_GA(X1)
FRONTD_IN_GA(tree(X1, X2, X3)) → PB_IN_GAGAA(X2, X3)
PB_IN_GAGAA(X1, X3) → U2_GAGAA(X1, X3, frontcD_in_ga(X1))
U2_GAGAA(X1, X3, frontcD_out_ga(X1, X2)) → FRONTD_IN_GA(X3)

The TRS R consists of the following rules:

frontcD_in_ga(void) → frontcD_out_ga(void, [])
frontcD_in_ga(tree(X1, void, void)) → frontcD_out_ga(tree(X1, void, void), .(X1, []))
frontcD_in_ga(tree(X1, X2, X3)) → U24_ga(X1, X2, X3, qcB_in_gagaa(X2, X3))
qcB_in_gagaa(X1, X3) → U21_gagaa(X1, X3, frontcD_in_ga(X1))
U21_gagaa(X1, X3, frontcD_out_ga(X1, X2)) → U22_gagaa(X1, X2, X3, frontcD_in_ga(X3))
U22_gagaa(X1, X2, X3, frontcD_out_ga(X3, X4)) → U23_gagaa(X1, X2, X3, X4, appcC_in_gga(X2, X4))
appcC_in_gga([], X1) → appcC_out_gga([], X1, X1)
appcC_in_gga(.(X1, X2), X3) → U25_gga(X1, X2, X3, appcC_in_gga(X2, X3))
U25_gga(X1, X2, X3, appcC_out_gga(X2, X3, X4)) → appcC_out_gga(.(X1, X2), X3, .(X1, X4))
U23_gagaa(X1, X2, X3, X4, appcC_out_gga(X2, X4, X5)) → qcB_out_gagaa(X1, X2, X3, X4, X5)
U24_ga(X1, X2, X3, qcB_out_gagaa(X2, X5, X3, X6, X4)) → frontcD_out_ga(tree(X1, X2, X3), X4)

The set Q consists of the following terms:

frontcD_in_ga(x0)
qcB_in_gagaa(x0, x1)
U21_gagaa(x0, x1, x2)
U22_gagaa(x0, x1, x2, x3)
appcC_in_gga(x0, x1)
U25_gga(x0, x1, x2, x3)
U23_gagaa(x0, x1, x2, x3, x4)
U24_ga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • FRONTD_IN_GA(tree(X1, X2, X3)) → PB_IN_GAGAA(X2, X3)
    The graph contains the following edges 1 > 1, 1 > 2

  • PB_IN_GAGAA(X1, X3) → FRONTD_IN_GA(X1)
    The graph contains the following edges 1 >= 1

  • PB_IN_GAGAA(X1, X3) → U2_GAGAA(X1, X3, frontcD_in_ga(X1))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U2_GAGAA(X1, X3, frontcD_out_ga(X1, X2)) → FRONTD_IN_GA(X3)
    The graph contains the following edges 2 >= 1

(27) YES